i, a, x:Id, X:Type, x0:X, P:(X), p:FinProbSpace, es:ES. pre-init1-p(es;i;x;X;x0;a;p;P)   

latex

Definitions	{T}, SQType(T), e loc e' , P  Q, e'e.P(e'), e@i. P(e), A c B, x:A. B(x), P  Q, P & Q, pre-init1-p(es;i;x;X;x0;a;p;P), , t  T, x:A. B(x)
Lemmas	Id wf, bool wf, finite-prob-space wf, event system wf, es-le-loc, Id sq, es-after wf, not wf, es-locl wf, es-vartype wf, es-when wf, es-loc wf, es-E wf, assert wf